(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_NRA)
(declare-fun v0 () Real)
(declare-fun v1 () Real)
(assert (let ((e2 1))
(let ((e3 6))
(let ((e4 (- v1 v0)))
(let ((e5 (* e4 v0)))
(let ((e6 (/ e2 (- e2))))
(let ((e7 (+ v0 e6)))
(let ((e8 (- e4)))
(let ((e9 (- e8 e7)))
(let ((e10 (* (- e2) e4)))
(let ((e11 (- v0 e5)))
(let ((e12 (- e8 e6)))
(let ((e13 (* e11 e6)))
(let ((e14 (+ e6 e11)))
(let ((e15 (- v0 e14)))
(let ((e16 (- e4 v0)))
(let ((e17 (/ e2 e2)))
(let ((e18 (* e11 (- e2))))
(let ((e19 (+ e7 e11)))
(let ((e20 (- e14 e4)))
(let ((e21 (+ e11 e13)))
(let ((e22 (+ e13 e21)))
(let ((e23 (/ e2 (- e2))))
(let ((e24 (* e12 e2)))
(let ((e25 (- e17 e21)))
(let ((e26 (* e3 e11)))
(let ((e27 (= e17 e6)))
(let ((e28 (distinct e23 e20)))
(let ((e29 (>= e7 e10)))
(let ((e30 (> e25 v0)))
(let ((e31 (< e26 e14)))
(let ((e32 (< e18 e13)))
(let ((e33 (>= e14 v1)))
(let ((e34 (<= e12 e21)))
(let ((e35 (= e15 e22)))
(let ((e36 (= e13 e24)))
(let ((e37 (>= e24 e20)))
(let ((e38 (distinct e20 e18)))
(let ((e39 (distinct e12 e19)))
(let ((e40 (= e26 e15)))
(let ((e41 (< e11 e4)))
(let ((e42 (>= e20 e26)))
(let ((e43 (> e16 e16)))
(let ((e44 (< e7 e7)))
(let ((e45 (distinct e5 e7)))
(let ((e46 (= e15 e13)))
(let ((e47 (> e24 e26)))
(let ((e48 (>= e25 v0)))
(let ((e49 (= e16 e24)))
(let ((e50 (distinct e17 e14)))
(let ((e51 (>= e23 e15)))
(let ((e52 (= e11 e11)))
(let ((e53 (> e18 e22)))
(let ((e54 (> e18 e7)))
(let ((e55 (>= e25 e12)))
(let ((e56 (> e18 e5)))
(let ((e57 (>= e8 e4)))
(let ((e58 (distinct e4 e10)))
(let ((e59 (> e23 e13)))
(let ((e60 (> e8 e4)))
(let ((e61 (distinct e16 e15)))
(let ((e62 (< e4 e8)))
(let ((e63 (> e11 v0)))
(let ((e64 (> e9 e9)))
(let ((e65 (> e5 e5)))
(let ((e66 (<= e14 v0)))
(let ((e67 (= e7 e24)))
(let ((e68 (>= e24 e9)))
(let ((e69 (distinct e17 e16)))
(let ((e70 (<= e6 e21)))
(let ((e71 (<= e22 e23)))
(let ((e72 (> e10 e21)))
(let ((e73 (= v1 e14)))
(let ((e74 (<= e26 e5)))
(let ((e75 (>= e18 e12)))
(let ((e76 (= e4 e6)))
(let ((e77 (distinct e17 e10)))
(let ((e78 (<= v1 e7)))
(let ((e79 (>= v1 v1)))
(let ((e80 (<= v1 e18)))
(let ((e81 (< e18 v1)))
(let ((e82 (= e25 e9)))
(let ((e83 (>= e21 e24)))
(let ((e84 (< e6 e8)))
(let ((e85 (>= e8 e25)))
(let ((e86 (distinct e4 e15)))
(let ((e87 (> e10 v1)))
(let ((e88 (<= e12 e7)))
(let ((e89 (distinct e21 e16)))
(let ((e90 (distinct e11 e23)))
(let ((e91 (<= e24 e12)))
(let ((e92 (< e4 e11)))
(let ((e93 (<= e18 e23)))
(let ((e94 (< e8 e21)))
(let ((e95 (<= e26 e16)))
(let ((e96 (> e5 e14)))
(let ((e97 (= e6 v1)))
(let ((e98 (>= e5 e23)))
(let ((e99 (= e10 e11)))
(let ((e100 (<= e20 e25)))
(let ((e101 (distinct e7 e22)))
(let ((e102 (= e10 e11)))
(let ((e103 (> e20 e17)))
(let ((e104 (< e12 e6)))
(let ((e105 (<= e4 e11)))
(let ((e106 (distinct e21 e20)))
(let ((e107 (>= e17 e19)))
(let ((e108 (< e11 v0)))
(let ((e109 (= e21 e12)))
(let ((e110 (<= e16 e17)))
(let ((e111 (distinct v0 e12)))
(let ((e112 (= e6 e4)))
(let ((e113 (< v1 e4)))
(let ((e114 (>= e14 e7)))
(let ((e115 (< e20 e22)))
(let ((e116 (> e18 e22)))
(let ((e117 (< e4 e4)))
(let ((e118 (> e23 e5)))
(let ((e119 (>= e11 e20)))
(let ((e120 (distinct e13 e19)))
(let ((e121 (not e30)))
(let ((e122 (and e72 e103)))
(let ((e123 (= e110 e76)))
(let ((e124 (xor e45 e122)))
(let ((e125 (ite e79 e57 e107)))
(let ((e126 (or e106 e41)))
(let ((e127 (xor e93 e28)))
(let ((e128 (and e32 e58)))
(let ((e129 (not e101)))
(let ((e130 (=> e80 e63)))
(let ((e131 (= e35 e55)))
(let ((e132 (xor e34 e126)))
(let ((e133 (or e69 e69)))
(let ((e134 (=> e29 e71)))
(let ((e135 (not e92)))
(let ((e136 (ite e47 e95 e97)))
(let ((e137 (and e60 e44)))
(let ((e138 (not e127)))
(let ((e139 (xor e37 e100)))
(let ((e140 (ite e105 e49 e130)))
(let ((e141 (ite e115 e33 e121)))
(let ((e142 (ite e125 e51 e50)))
(let ((e143 (or e140 e104)))
(let ((e144 (=> e61 e134)))
(let ((e145 (ite e102 e84 e90)))
(let ((e146 (not e145)))
(let ((e147 (= e39 e74)))
(let ((e148 (= e48 e62)))
(let ((e149 (and e31 e96)))
(let ((e150 (= e64 e64)))
(let ((e151 (=> e59 e112)))
(let ((e152 (= e43 e117)))
(let ((e153 (=> e119 e38)))
(let ((e154 (not e70)))
(let ((e155 (ite e52 e36 e131)))
(let ((e156 (xor e123 e77)))
(let ((e157 (= e40 e113)))
(let ((e158 (= e141 e99)))
(let ((e159 (not e154)))
(let ((e160 (and e138 e109)))
(let ((e161 (=> e85 e152)))
(let ((e162 (= e116 e142)))
(let ((e163 (and e94 e132)))
(let ((e164 (ite e139 e136 e159)))
(let ((e165 (or e88 e137)))
(let ((e166 (not e128)))
(let ((e167 (and e114 e150)))
(let ((e168 (ite e167 e65 e53)))
(let ((e169 (not e108)))
(let ((e170 (not e56)))
(let ((e171 (= e157 e165)))
(let ((e172 (and e164 e27)))
(let ((e173 (xor e118 e172)))
(let ((e174 (=> e143 e162)))
(let ((e175 (=> e89 e166)))
(let ((e176 (xor e144 e75)))
(let ((e177 (=> e151 e82)))
(let ((e178 (and e46 e87)))
(let ((e179 (ite e146 e146 e66)))
(let ((e180 (not e148)))
(let ((e181 (ite e156 e156 e180)))
(let ((e182 (ite e83 e78 e98)))
(let ((e183 (or e174 e73)))
(let ((e184 (or e160 e168)))
(let ((e185 (=> e120 e111)))
(let ((e186 (not e183)))
(let ((e187 (not e54)))
(let ((e188 (ite e42 e185 e153)))
(let ((e189 (or e133 e133)))
(let ((e190 (xor e129 e181)))
(let ((e191 (=> e175 e135)))
(let ((e192 (= e178 e188)))
(let ((e193 (and e169 e173)))
(let ((e194 (= e182 e158)))
(let ((e195 (xor e161 e192)))
(let ((e196 (ite e170 e186 e176)))
(let ((e197 (or e177 e191)))
(let ((e198 (xor e179 e190)))
(let ((e199 (or e68 e124)))
(let ((e200 (and e155 e184)))
(let ((e201 (not e200)))
(let ((e202 (xor e91 e197)))
(let ((e203 (ite e171 e194 e193)))
(let ((e204 (= e198 e81)))
(let ((e205 (xor e86 e86)))
(let ((e206 (xor e202 e163)))
(let ((e207 (not e195)))
(let ((e208 (= e67 e196)))
(let ((e209 (and e149 e201)))
(let ((e210 (= e204 e203)))
(let ((e211 (= e210 e210)))
(let ((e212 (ite e205 e147 e187)))
(let ((e213 (not e207)))
(let ((e214 (or e213 e211)))
(let ((e215 (= e208 e212)))
(let ((e216 (not e214)))
(let ((e217 (and e189 e199)))
(let ((e218 (xor e216 e216)))
(let ((e219 (and e209 e206)))
(let ((e220 (and e217 e217)))
(let ((e221 (ite e215 e215 e215)))
(let ((e222 (=> e220 e220)))
(let ((e223 (ite e219 e221 e222)))
(let ((e224 (not e218)))
(let ((e225 (and e223 e223)))
(let ((e226 (not e225)))
(let ((e227 (= e224 e226)))
e227
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
